Modal Homotopy Type Theory

FROM: Максим Сохацький
TO: Формальна Філософія

Тут представлена анотація на книгу Девіда Корфілда "Модальна Гомотопочна Теорія Типів. Перспектива нової логіки для філософії".

Модальна гомотопічна теорія типів --- це сучасне поєднання модальної теорії типів (для вираження або класичних модальних логік висловлювань К, S4, S5 і т.д. або сучасних (ко)-монадичних інтерпретаторів які реалізують відповідні модальності) з та у застосуванні до гомотопічної теорії типів. Це поєднання мотивовано багатьма дослідженнями та відкритими проблемами одна з яких це неможливість реалізації доведення Брауера про нерухому точку у чистій HoTT. До цього модальності в теоретичній інформатиці моделювалося за допомогою семантик Кріпке, тому перехід до категорної моделі монад або роботі в 2-теорії типів, дав змогу формалізації інфінітіземальних околів та понять многовидів у алгебраїчній геометрії.

Крім метатеоретичної частини у зв'язаних топосах та геометричних морфізмах між ними, сформульованої Вільямом Ловером, автор показує також основи залежної теорії типів, та її застосування до філософії та формальної природньої людської мови. На мою думку потужна логічна основа та формальна модель NLP --- це запорука успішної системи обробки природньої мови гомосапієнсів побудованої на стохастичних моделях.

Найприємніше в книзі є те, що значна її частина приділяється історії виникнення модальної HoTT як результату пошуку формальної моделі для калібрувальної інваріантністі (теоретична фізика) Урсом Шрайбером. Відповідь на цей запит спочатку була представлена Майклом Шульманом як cohesivett, а пізніше, на Конференції по диференціальній геометорії в модальній HoTT влаштованій Феліксом Велленом, на якій мені довелось побувати, і саме конструктивне доведення теореми Брауера про нерухому точку в модальній HoTT. Детальний звіт про конференцію.

Модальності важливі не тільки для застосувані у формалізації часу в природній мові, та геометричного поняття коіндуктивного околу, або дійсних чисел, модальності також формалізують поняття процесу, як фізичного так і інформатико-теоретичного. Позаяк числення процесів цілком поглинається модальною теорією типів у зв'язаних топосах, модальна HoTT у свою чергу не тільки забезпечує формалізацію теоретичної фізики, але і відкриває двері у формальну філософію різних модальностей, або інтерпретацій.

Зараз ♭-модальність уже вбудована в Агду, та існують уже прототипи мультимодальних тайпчекерів. Раджу цю книжку усім математикам, усім програмістам, та усім філософам у якості підручника з формальної філософії.